Formal spec alignment for GitHub MCP access-control conformance docs and predicate mapping by Copilot · Pull Request #47633 · github/gh-aw

Copilot · 2026-07-23T16:13:37Z

This updates the formal-spec artifacts for GitHub MCP access-control compliance so the documented model, coverage map, and execution instructions stay synchronized with the executable conformance suite. It also corrects a predicate label mismatch in the formal test commentary to match the defined P1–P6 ordering.

Spec usage contract alignment
- Replaced the generic “Running Compliance Tests” section with a focused Usage section in specs/github-mcp-access-control-compliance/README.md.
- Usage now explicitly reflects the formal suite entrypoints and self-contained test-file contract.
Predicate mapping consistency
- Corrected the inline predicate reference in TestFormal_OmittedReposAllowAll from P1_RepoMatch to P2_RepoMatch in pkg/workflow/github_mcp_access_control_formal_test.go, matching the formal guard ordering (P1=ToolAllowed, P2=RepoMatch).

Example of the corrected predicate annotation:

func TestFormal_OmittedReposAllowAll(t *testing.T) {
	// P2_RepoMatch: omitted repos field means "no restriction" — all accessible repos are allowed (spec §4.4.1).
	...
}

Fixes [formal-spec] github-mcp-access-control-compliance/README.md — Formal model & test suite — 2026-07-23 #47632

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

github-actions · 2026-07-23T18:44:42Z

🤖 PR Triage

Field	Value
Category	`docs`
Risk	🟡 Medium
Priority Score	50/100
Recommended Action	`batch_review`

Score breakdown: Impact 20 + Urgency 15 + Quality 15

Batch: batch-spec-docs with #47637

Rationale: Draft PR updating formal spec for GitHub MCP access-control compliance. Only 2 files (a Go test + README). No CI data. Groups with #47637 for a doc/spec batch review.

Generated by 🔧 PR Triage Agent · sonnet46 · 38.1 AIC · ⌖ 6.75 AIC · ⊞ 5.7K · ◷

github-actions · 2026-07-23T21:19:30Z

Great work on keeping the formal spec artifacts and conformance suite synchronized! 🎯 This correction to the predicate label mapping (P2_RepoMatch) and the Usage section update in the compliance README are important for maintainability.

Here's one thing that would strengthen this PR:

Add conformance tests — The predicate mapping correction in TestFormal_OmittedReposAllowAll would benefit from additional test cases to verify the P1–P6 ordering holds across boundary conditions. Consider adding tests that exercise the redefined predicate sequence to ensure the fix is durable.

If you'd like to enhance this, you can assign this prompt to your coding agent:

Add unit tests for the GitHub MCP access-control formal predicate ordering (P1–P6) in pkg/workflow/github_mcp_access_control_formal_test.go.

The tests should verify:
1. P1 (ToolAllowed) evaluation occurs before P2 (RepoMatch)
2. When a repo is omitted, P2_RepoMatch correctly allows all accessible repos
3. The predicate sequence is consistent across all guard conditions

Ensure tests cover both positive cases (predicates pass) and negative cases (predicates fail at the expected stage).

Generated by ✅ Contribution Check · sonnet46 · 63.6 AIC · ⌖ 11 AIC · ⊞ 6.2K · ◷

github-actions · 2026-07-24T00:57:09Z

🤖 PR Triage — §30057272009

Field	Value
Category	`docs`
Risk	🟢 Low
Priority Score	28 / 100
Action	⏸ `defer`
CI	⬜ None (draft)
Review	None
Batch	`spec-docs`

Score breakdown: Impact 20 + Urgency 5 + Quality 3

Rationale: DRAFT PR. Formal spec alignment docs only. No CI, no reviews. Defer until undrafted and CI passes.

Next action: Undraft, ensure CI passes, then consider merging alongside #47637.

Generated by 🔧 PR Triage Agent · sonnet46 · 35.7 AIC · ⌖ 5.3 AIC · ⊞ 5.7K · ◷

github-actions · 2026-07-24T02:56:02Z

🧠 Matt Pocock Skills Reviewer has completed the skills-based review. ✅

github-actions · 2026-07-24T02:56:03Z

✅ Test Quality Sentinel completed test quality analysis.

No new or modified test functions detected. The PR only updates a comment ('P1_RepoMatch' → 'P2_RepoMatch') in an existing test. Test Quality Sentinel skipped.

github-actions · 2026-07-24T02:56:08Z

✅ PR Code Quality Reviewer completed the code quality review.

Copilot

Pull request overview

Aligns formal access-control documentation and predicate annotations with the executable conformance suite.

Changes:

Updates usage instructions for running formal tests.
Corrects the repository predicate label from P1 to P2.

Show a summary per file

File	Description
`specs/github-mcp-access-control-compliance/README.md`	Documents formal suite entrypoints and test-file contract.
`pkg/workflow/github_mcp_access_control_formal_test.go`	Corrects the omitted-repository predicate annotation.

Review details

Tip

Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Files reviewed: 2/2 changed files
Comments generated: 0
Review effort level: Medium

github-actions · 2026-07-24T02:56:34Z

✅ Design Decision Gate 🏗️ completed the design decision gate check.

No ADR enforcement needed: PR does not have the 'implementation' label and has ≤100 new lines of code in business logic directories (default_business_additions=1).

github-actions

No blocking issues. The predicate label correction (P1_RepoMatch to P2_RepoMatch) is accurate per the documented ordering (P1=ToolAllowed, P2=RepoMatch), and the README simplification is clean.

🔎 Code quality review by PR Code Quality Reviewer · sonnet46 · 13.2 AIC · ⌖ 4.46 AIC · ⊞ 5.7K
_{Comment /review to run again}

github-actions

Review

Changes look correct.

Predicate fix: P1_RepoMatch → P2_RepoMatch is accurate given the defined ordering (P1=ToolAllowed, P2=RepoMatch).
README simplification: Replacing the explicit long regex with TestFormal_ prefix is cleaner and future-proof as new tests are added.

Minor note: the removal of the TestValidateGitHubGuardPolicy run instructions from the README reduces discoverability for those §11.1.x tests, but this is a deliberate scope decision and not blocking.

🧵 Reviewed using Impeccable skills by Impeccable Skills Reviewer · sonnet46 · 18.1 AIC · ⌖ 4.49 AIC · ⊞ 5K

github-actions

Skills-Based Review 🧠

Applied /grill-with-docs — this is a clean, focused documentation and comment-fix PR. Approving.

📋 Summary

What changed

Predicate label fix (P1_RepoMatch → P2_RepoMatch in TestFormal_OmittedReposAllowAll): Correctly aligns with the formal guard ordering defined in the spec (P1=ToolAllowed, P2=RepoMatch). Verified against the spec README lines 23–43.
README simplification: Replaced a fragile exhaustive test-name list with the simpler TestFormal_ prefix pattern, which is less likely to drift as new tests are added.

Positive Highlights

✅ Predicate fix is accurate and traceable to the spec definition
✅ Simplified go test -run "TestFormal_" pattern is less fragile than the old exhaustive named list
✅ Numbered steps in the Usage section improve readability

🧠 Reviewed using Matt Pocock's skills by Matt Pocock Skills Reviewer · sonnet46 · 26.8 AIC · ⌖ 4.55 AIC · ⊞ 6.7K
_{Comment /matt to run again}

…l-compliance

pelikhan · 2026-07-24T04:20:26Z

@copilot run pr-finishser skill

Initial plan

ba4657d

Copilot AI assigned Copilot and pelikhan Jul 23, 2026

Copilot started work on behalf of pelikhan July 23, 2026 16:14 View session

Copilot AI linked an issue Jul 23, 2026 that may be closed by this pull request

[formal-spec] github-mcp-access-control-compliance/README.md — Formal model & test suite — 2026-07-23 #47632

Closed

Align formal access-control spec usage and predicate label

0d9f0c6

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

Copilot AI changed the title ~~[WIP] Add formal model and test suite for GitHub MCP access control compliance~~ Formal spec alignment for GitHub MCP access-control conformance docs and predicate mapping Jul 23, 2026

Copilot finished work on behalf of pelikhan July 23, 2026 16:26

Copilot AI requested a review from pelikhan July 23, 2026 16:26

github-actions Bot mentioned this pull request Jul 23, 2026

[Contribution Check Report] Contribution Check — 2026-07-23 #47444

Closed

github-actions Bot mentioned this pull request Jul 23, 2026

Close SPDD conformance gaps for ADRs 27325/27327/27387/27476/27479 #47637

Merged

github-actions Bot added pr-action:batch_review pr-agent:copilot pr-batch:spec-docs pr-priority:medium pr-risk:medium pr-type:docs labels Jul 23, 2026

github-actions Bot added pr-action:defer pr-priority:low pr-risk:low labels Jul 24, 2026

pelikhan marked this pull request as ready for review July 24, 2026 02:54

Copilot AI review requested due to automatic review settings July 24, 2026 02:54

Copilot started reviewing on behalf of pelikhan July 24, 2026 02:55 View session

Copilot AI reviewed Jul 24, 2026

View reviewed changes

github-actions Bot approved these changes Jul 24, 2026

View reviewed changes

This was referenced Jul 24, 2026

[aw] Matt Pocock Skills Reviewer failed #47685

Open

[pr-sous-chef] pr-sous-chef run report #47673

Open

Merge branch 'main' into copilot/formal-spec-github-mcp-access-contro…

a3ab164

…l-compliance

Copilot started work on behalf of pelikhan July 24, 2026 04:21 View session

pelikhan merged commit 1192d44 into main Jul 24, 2026
23 of 24 checks passed

pelikhan deleted the copilot/formal-spec-github-mcp-access-control-compliance branch July 24, 2026 04:29

Copilot stopped work on behalf of pelikhan due to an error July 24, 2026 04:29
The session was cancelled by the user.

This was referenced Jul 24, 2026

[aw] No-Op Runs #43499

Open

Smoke Test: MAI-Code-1-Flash - 30069261871 #47709

Open

Uh oh!

Conversation

Copilot AI commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 23, 2026

🤖 PR Triage

Uh oh!

github-actions Bot commented Jul 23, 2026

Uh oh!

github-actions Bot commented Jul 24, 2026

🤖 PR Triage — §30057272009

Uh oh!

github-actions Bot commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Review details

Uh oh!

github-actions Bot commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Review

Uh oh!

github-actions Bot left a comment

Choose a reason for hiding this comment

Skills-Based Review 🧠

What changed

Positive Highlights

Uh oh!

pelikhan commented Jul 24, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Copilot AI commented Jul 23, 2026 •

edited

Loading

github-actions Bot commented Jul 24, 2026 •

edited

Loading

github-actions Bot commented Jul 24, 2026 •

edited

Loading

github-actions Bot commented Jul 24, 2026 •

edited

Loading

github-actions Bot commented Jul 24, 2026 •

edited

Loading